\Slide{LockCountAnalysis design}{
\B
\item Java monitor locks are recursive:
      can be acquired multiple times
\item Dataflow fact is an integer count
\item When {\tt monitorenter} is executed, increment count
\item When {\tt monitorexit} is executed, decrement count
\item javac ensures that a lock is released no matter
      how control leaves a {\tt synchronized} block
  \B
  \item So, we should see proper balancing of 
        {\tt monitorenter} / {\tt monitorexit}
  \E
\E
}
